FLAT.PRF[W82,JMC]1 - www.SailDart.org

perm filename FLAT.PRF[W82,JMC]1 blob sn#635469 filedate 1982-01-19 generic text, type T, neo UTF8
(VERS1 0 (NIL ((LINENAME LISTPFLATTEN (LN& #& . 0)) (LINENAME SORTINFO (LN& #& . 18) (LN& #& . 58) (LN& #& . 40) (LN& #& . 41) (LN& #& . 48) (LN& #& . 49) (LN& #& . 54) (LN& #& . 50)) (LINENAME SIMPINFO (LN& #& . 58) (LN& #& . 59) (LN& #& . 62) (LN& #& . 63) (LN& #& . 64) (LN& #& . 70) (LN& #& . 71) (LN& #& . 72) (LN& #& . 73) (LN& #& . 74) (LN& #& . 75) (LN& #& . 76) (LN& #& . 77)) (LINENAME CONSFACTS (LN& #& . 62) (LN& #& . 63) (LN& #& . 71) (LN& #& . 72)) (LINENAME LISTINDUCTION (LN& #& . 99)) (LINENAME SEXPINDUCTION (LN& #& . 1)) (LINENAME LISTAPPEND (LN& #& . 54)) (LINENAME DEFINFO (LN& #& . 78) (LN& #& . 79) (LN& #& . 89) (LN& #& . 92) (LN& #& . 93) (LN& #& . 96)) (LINENAME APPENDFACTS (LN& #& . 76) (LN& #& . 77)) (LINENAME REVERSEAPPEND (LN& #& . 100))) (FLAT (#& . 95) (#& . 93) (#& . 101) (#& . 98) (#& . 96) (#& . 102) (#& . 103) (#& . 0) (#& . 104) (#& . 105) (#& . 106) (#& . 107) (#& . 108) (#& . 109) (#& . 110) (#& . 111) (#& . 112) (#& . 113) (#& . 114) (#& . 115) (#& . 116) (#& . 117) (#& . 118) (#& . 119) (#& . 120) (#& . 121) (#& . 122) (#& . 123) (#& . 124) (#& . 125) (#& . 126)) (LISPAX (#& . 20) (#& . 13) (#& . 127) (#& . 11) (#& . 61) (#& . 131) (#& . 8) (#& . 66) (#& . 3) (#& . 46) (#& . 38) (#& . 18) (#& . 133) (#& . 58) (#& . 134) (#& . 135) (#& . 59) (#& . 136) (#& . 40) (#& . 137) (#& . 62) (#& . 138) (#& . 63) (#& . 139) (#& . 64) (#& . 140) (#& . 70) (#& . 141) (#& . 71) (#& . 142) (#& . 72) (#& . 143) (#& . 99) (#& . 144) (#& . 1) (#& . 145) (#& . 43) (#& . 41) (#& . 146) (#& . 73) (#& . 147) (#& . 48) (#& . 148) (#& . 74) (#& . 149) (#& . 49) (#& . 150) (#& . 75) (#& . 151) (#& . 56) (#& . 54) (#& . 152) (#& . 78) (#& . 153) (#& . 76) (#& . 154) (#& . 77) (#& . 155) (#& . 81) (#& . 88) (#& . 79) (#& . 156) (#& . 91) (#& . 89) (#& . 157) (#& . 52) (#& . 50) (#& . 158) (#& . 92) (#& . 159) (#& . 100) (#& . 160) (#& . 161))) ((((∀ U)) (= (REVERSE (REVERSE U)) U)) . (AXIOM (TM& ((∀ U)) (= (REVERSE (REVERSE U)) U))) . NIL . ((REVERSE #& . 51) (U #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 73 .) (NIL . (COMMENTL LNAME REVERSEAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 72 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 70 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 68 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 65 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 62 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 58 .) (NIL . (COMMENTL LNAME APPENDFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 56 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 54 .) (NIL . (COMMENTL LNAME SORTINFO LISTAPPEND) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 52 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 49 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 47 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 45 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 43 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 41 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 39 .) (NIL . (COMMENTL LNAME SEXPINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 36 .) (NIL . (COMMENTL LNAME LISTINDUCTION) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 34 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 32 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 30 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 28 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 26 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 24 .) (NIL . (COMMENTL LNAME CONSFACTS SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 22 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 20 .) (NIL . (COMMENTL LNAME SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 18 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡ (NULL U) (= U NNIL)))) . NIL . ((U #& . 19) (NNIL #& . 60) (NULL #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 16 .) (NIL . (COMMENTL LNAME SORTINFO SIMPINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 15 .) (NIL . (COMMENTL LNAME SORTINFO) . NIL . NIL . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 13 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 131) . CONS .) (NIL . (DECL (CONS) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((CONS #& . 132)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 6 .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 127) . B .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 127) . A .) (VARIABLE . GROUND . UNIVERSAL . NIL . NIL . (#& . 127) . C .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((C #& . 128) (A #& . 129) (B #& . 130)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 3 .) ((((∀ X U)) (LISTP (FLAT X U))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) (STANDARD) ((PART ((1 2 1 2))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD) ((PART ((1))) DER) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((X #& . 12) (U #& . 19) (LISTP #& . 45) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 31 .) ((⊃ (((∀ X Y)) (CONDI (ATOM (~ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (~ (~ X Y) U)))) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (CAR (~ X Y)) (FLAT (CDR (~ X Y)) U))))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (CDR #& . 67) (CAR #& . 65) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 30 .) ((⊃ (((∀ X Y)) (CONDI (ATOM (~ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (~ (~ X Y) U)))) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (CAR (~ X Y)) (FLAT (CDR (~ X Y)) U))))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (CDR #& . 67) (CAR #& . 65) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 29 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (CONDI (ATOM (~ X Y)) (((∀ U)) (LISTP (~ (~ X Y) U))) (((∀ U)) (LISTP (FLAT (CAR (~ X Y)) (FLAT (CDR (~ X Y)) U))))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD))) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (CDR #& . 67) (CAR #& . 65) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 28 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (~ X Y) U))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD)) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 27 .) ((⊃ (∧ (((∀ X)) TRUE) (((∀ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (~ X Y) U)))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD))) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 26 .) ((⊃ (∧ (((∀ X)) (⊃ (ATOM X) (((∀ U)) (LISTP (~ X U))))) (((∀ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (~ X Y) U)))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) (STANDARD))) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 25 .) ((⊃ (∧ (((∀ X)) (⊃ (ATOM X) (((∀ U)) (LISTP (CONDI (ATOM X) (~ X U) (FLAT (CAR X) (FLAT (CDR X) U))))))) (((∀ X Y)) (⊃ (∧ (((∀ U)) (LISTP (FLAT X U))) (((∀ U)) (LISTP (FLAT Y U)))) (((∀ U)) (LISTP (FLAT (~ X Y) U)))))) (((∀ X U)) (LISTP (FLAT X U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)))) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (U #& . 19) (LISTP #& . 45) (CDR #& . 67) (CAR #& . 65) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 24 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (CONDI FALSE (~ (~ X Y) U) (FLAT X (FLAT Y U))) (* (CONDI FALSE (~ (~ X Y) NNIL) (* (FLATTEN X) (FLATTEN Y))) U))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)))) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (NNIL #& . 60) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 23 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) (STANDARD)) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 22 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) ($ LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) (STANDARD)) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 21 .) ((⊃ (∧ (((∀ X)) TRUE) (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U)))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) ($ LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD))) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 20 .) ((⊃ (∧ (((∀ X)) (CONDI (NULL (~ X NNIL)) (⊃ (ATOM X) (((∀ U)) (= (~ X U) U))) (⊃ (ATOM X) (((∀ U)) (= (~ X U) (~ (CAR (~ X NNIL)) (* (CDR (~ X NNIL)) U))))))) (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U)))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) ($ LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD))) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (NULL #& . 4) (CDR #& . 67) (CAR #& . 65) (NNIL #& . 60) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 19 .) ((⊃ (∧ (((∀ X)) (⊃ (ATOM X) (((∀ U)) (= (~ X U) (* (~ X NNIL) U))))) (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U)))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) ($ LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD))) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (NNIL #& . 60) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 18 .) ((⊃ (∧ (((∀ X)) (⊃ (ATOM X) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))))) (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT (~ X Y) U) (* (FLATTEN (~ X Y)) U)))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& STANDARD) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((ATOM #& . 2) (~ #& . 7) (X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50)) . NIL . FLAT . NIL . NIL . 17 .) ((((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U))) . (TRW (TM& ((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U))) (MODE& * (IMP LR& (#& . 105) (#& . 110)) (TAUT))) . NIL . ((X #& . 12) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 50) (#& . 54) (#& . 49) (#& . 48) (#& . 41) (#& . 40) (#& . 58) (#& . 18) (#& . 96) (#& . 93) (#& . 92) (#& . 89) (#& . 79) (#& . 78) (#& . 77) (#& . 76) (#& . 75) (#& . 74) (#& . 73) (#& . 72) (#& . 71) (#& . 70) (#& . 64) (#& . 63) (#& . 62) (#& . 59) (#& . 1)) . NIL . FLAT . NIL . NIL . 16 .) ((((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT X (FLAT Y U)) (* (FLATTEN X) (FLATTEN Y) U))))) . (∀I (X Y) (LN& #& . 109)) . NIL . ((X #& . 12) (FLATTEN #& . 97) (U #& . 19) (Y #& . 17) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 50) (#& . 54) (#& . 49) (#& . 48) (#& . 41) (#& . 40) (#& . 58) (#& . 18) (#& . 96) (#& . 93) (#& . 92) (#& . 89) (#& . 79) (#& . 78) (#& . 77) (#& . 76) (#& . 75) (#& . 74) (#& . 73) (#& . 72) (#& . 71) (#& . 70) (#& . 64) (#& . 63) (#& . 62) (#& . 59) (#& . 1)) . NIL . FLAT . NIL . NIL . 15 .) ((⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT X (FLAT Y U)) (* (FLATTEN X) (FLATTEN Y) U)))) . (CI ((LR& (#& . 106))) (LN& #& . 108) (MODE& STANDARD)) . NIL . ((X #& . 12) (FLATTEN #& . 97) (U #& . 19) (Y #& . 17) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 50) (#& . 54) (#& . 49) (#& . 48) (#& . 41) (#& . 40) (#& . 58) (#& . 18) (#& . 96) (#& . 93) (#& . 92) (#& . 89) (#& . 79) (#& . 78) (#& . 77) (#& . 76) (#& . 75) (#& . 74) (#& . 73) (#& . 72) (#& . 71) (#& . 70) (#& . 64) (#& . 63) (#& . 62) (#& . 59) (#& . 1)) . NIL . FLAT . NIL . NIL . 14 .) ((((∀ U)) (= (FLAT X (FLAT Y U)) (* (FLATTEN X) (* (FLATTEN Y) U)))) . (∀I (U) (LN& #& . 107)) . NIL . ((X #& . 12) (FLATTEN #& . 97) (U #& . 19) (Y #& . 17) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 106)) . NIL . FLAT . NIL . NIL . 13 .) ((= (FLAT X (FLAT Y U)) (* (FLATTEN X) (* (FLATTEN Y) U))) . (TRW (TM& FLAT X (FLAT Y U)) (MODE& REC LR& (#& . 106)) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((X #& . 12) (FLATTEN #& . 97) (U #& . 19) (Y #& . 17) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 106)) . NIL . FLAT . NIL . NIL . 12 .) ((∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) . (ASSUME (TM& ∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U))))) . NIL . ((X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . FLAT . NIL . NIL . 11 .) ((⊃ (((∀ X Y)) (⊃ (∧ (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U))) (((∀ U)) (= (FLAT Y U) (* (FLATTEN Y) U)))) (((∀ U)) (= (FLAT X (FLAT Y U)) (* (FLATTEN X) (FLATTEN Y) U))))) (((∀ X U)) (= (FLAT X U) (* (FLATTEN X) U)))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (= (FLAT X U) (* (FLATTEN X) U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD))) (LR& (#& . 0) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((X #& . 12) (Y #& . 17) (FLATTEN #& . 97) (U #& . 19) (FLAT #& . 94)) . ((* #& . 55)) . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 10 .) (NIL . (COMMENTL LNAME LISTPFLATTEN) . NIL . NIL . NIL . NIL . NIL . NIL . FLAT . NIL . NIL . 9 .) ((((∀ X U)) (LISTP (FLAT X U))) . (∀E PHI (TM& ((λ X)) (((∀ U)) (LISTP (FLAT X U)))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) (STANDARD) ((PART ((1 2 1 2))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (REC LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD) ((PART ((1))) DER) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((X #& . 12) (U #& . 19) (LISTP #& . 45) (FLAT #& . 94)) . NIL . NIL . ((#& . 1) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 7 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . FLAT . NIL . NIL . 6 .) (NIL . (COMMENTL LNAME DEFINFO) . NIL . NIL . NIL . NIL . NIL . NIL . FLAT . NIL . NIL . 3 .) ((((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U)))) . (AXIOM (TM& ((∀ U V)) (= (REVERSE (* U V)) (* (REVERSE V) (REVERSE U))))) . NIL . ((V #& . 32) (U #& . 19) (REVERSE #& . 51)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 71 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (~ X U))))) (((∀ U)) (PHI U))))) . NIL . ((U #& . 19) (X #& . 12) (PHI #& . 10) (NNIL #& . 60) (~ #& . 7)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 33 .) (NIL . (DECL (FLATTEN) (OT& (GROUND) . GROUND) CONSTANT) . NIL . ((FLATTEN #& . 97)) . NIL . NIL . NIL . NIL . FLAT . NIL . NIL . 4 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 98) . FLATTEN .) ((((∀ X)) (= (FLATTEN X) (CONDI (ATOM X) (LIST X) (* (FLATTEN (CAR X)) (FLATTEN (CDR X)))))) . (AXIOM (TM& ((∀ X)) (= (FLATTEN X) (CONDI (ATOM X) (LIST X) (* (FLATTEN (CAR X)) (FLATTEN (CDR X))))))) . NIL . ((CAR #& . 65) (CDR #& . 67) (ATOM #& . 2) (X #& . 12) (FLATTEN #& . 97)) . ((LIST #& . 42) (* #& . 55)) . NIL . ((&& . 1)) . NIL . FLAT . NIL . NIL . 5 .) (NIL . (DECL (FLAT) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((FLAT #& . 94)) . NIL . NIL . NIL . NIL . FLAT . NIL . NIL . 1 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 95) . FLAT .) ((((∀ X U)) (= (FLAT X U) (CONDI (ATOM X) (~ X U) (FLAT (CAR X) (FLAT (CDR X) U))))) . (AXIOM (TM& ((∀ X U)) (= (FLAT X U) (CONDI (ATOM X) (~ X U) (FLAT (CAR X) (FLAT (CDR X) U)))))) . NIL . ((X #& . 12) (ATOM #& . 2) (~ #& . 7) (CDR #& . 67) (CAR #& . 65) (U #& . 19) (FLAT #& . 94)) . NIL . NIL . ((&& . 1)) . NIL . FLAT . NIL . NIL . 2 .) ((((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U)))))) . (AXIOM (TM& ((∀ U)) (= (REVERSE U) (CONDI (NULL U) NNIL (* (REVERSE (CDR U)) (LIST (CAR U))))))) . NIL . ((REVERSE #& . 51) (NULL #& . 4) (CDR #& . 67) (CAR #& . 65) (NNIL #& . 60) (U #& . 19)) . ((LIST #& . 42) (* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 69 .) (NIL . (DECL (MEMBER) (OT& (GROUND GROUND) . TRUTHVAL) CONSTANT) . NIL . ((MEMBER #& . 90)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 63 .) (CONSTANT . ((GROUND GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 91) . MEMBER .) ((((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U)))))) . (AXIOM (TM& ((∀ X U)) (≡ (MEMBER X U) (∧ (¬ (NULL U)) (∨ (= X (CAR U)) (MEMBER X (CDR U))))))) . NIL . ((NULL #& . 4) (CDR #& . 67) (CAR #& . 65) (X #& . 12) (U #& . 19) (MEMBER #& . 90)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 64 .) (NIL . (DECL (ASSOC) (OT& (GROUND GROUND) . GROUND) CONSTANT) . NIL . ((ASSOC #& . 87)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 60 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . NIL . (#& . 88) . ASSOC .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A1 .) (6 . ALISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 85) . (#& . 81) . ALISTP .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A0 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . A2 .) (NIL . (DECL (ALIST A0 A1 A2) (OT& . GROUND) VARIABLE ALISTP) . NIL . ((A2 #& . 82) (A0 #& . 83) (ALISTP #& . 84) (ALIST #& . 80) (A1 #& . 86)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 59 .) (VARIABLE . GROUND . ALISTP . NIL . NIL . (#& . 81) . ALIST .) ((((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST)))))) . (AXIOM (TM& ((∀ X ALIST)) (= (ASSOC X ALIST) (CONDI (NULL ALIST) NNIL (CONDI (= X (CAR (CAR ALIST))) (CAR ALIST) (ASSOC X (CDR ALIST))))))) . NIL . ((X #& . 12) (NNIL #& . 60) (CAR #& . 65) (CDR #& . 67) (NULL #& . 4) (ALIST #& . 80) (ASSOC #& . 87)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 61 .) ((((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V) (CONDI (NULL U) V (~ (CAR U) (* (CDR U) V)))))) . NIL . ((NULL #& . 4) (CDR #& . 67) (CAR #& . 65) (~ #& . 7) (U #& . 19) (V #& . 32)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 53 .) ((((∀ X U V)) (= (* (~ X U) V) (~ X (* U V)))) . (AXIOM (TM& ((∀ X U V)) (= (* (~ X U) V) (~ X (* U V))))) . NIL . ((~ #& . 7) (X #& . 12) (U #& . 19) (V #& . 32)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 57 .) ((((∀ U)) (= (* NNIL U) U)) . (AXIOM (TM& ((∀ U)) (= (* NNIL U) U))) . NIL . ((U #& . 19) (NNIL #& . 60)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 55 .) ((((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z)))) . (AXIOM (TM& ((∀ X Y Z)) (= (LIST X Y Z) (~ X (LIST Y Z))))) . NIL . ((~ #& . 7) (Z #& . 14) (X #& . 12) (Y #& . 17)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 48 .) ((((∀ X Y)) (= (LIST X Y) (~ X (LIST Y)))) . (AXIOM (TM& ((∀ X Y)) (= (LIST X Y) (~ X (LIST Y))))) . NIL . ((~ #& . 7) (X #& . 12) (Y #& . 17)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 44 .) ((((∀ X)) (= (LIST X) (~ X NNIL))) . (AXIOM (TM& ((∀ X)) (= (LIST X) (~ X NNIL)))) . NIL . ((~ #& . 7) (NNIL #& . 60) (X #& . 12)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 40 .) ((((∀ X Y)) (= (CDR (~ X Y)) Y)) . (AXIOM (TM& ((∀ X Y)) (= (CDR (~ X Y)) Y))) . NIL . ((CDR #& . 67) (~ #& . 7) (X #& . 12) (Y #& . 17)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 31 .) ((((∀ X Y)) (= (CAR (~ X Y)) X)) . (AXIOM (TM& ((∀ X Y)) (= (CAR (~ X Y)) X))) . NIL . ((Y #& . 17) (X #& . 12) (~ #& . 7) (CAR #& . 65)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 29 .) ((((∀ X U)) (= (CDR (~ X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (~ X U)) U))) . NIL . ((CDR #& . 67) (~ #& . 7) (X #& . 12) (U #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 27 .) (4 . |CAR | . UNARY . 950 .) (4 . |CDR | . UNARY . 950 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 68) . (#& . 66) . CDR .) (NIL . (DECL (CAR CDR) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((CDR #& . 67) (CAR #& . 65)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 8 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 69) . (#& . 66) . CAR .) ((((∀ X U)) (= (CAR (~ X U)) X)) . (AXIOM (TM& ((∀ X U)) (= (CAR (~ X U)) X))) . NIL . ((U #& . 19) (X #& . 12) (~ #& . 7) (CAR #& . 65)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 25 .) ((((∀ X U)) (¬ (NULL (~ X U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (~ X U))))) . NIL . ((NULL #& . 4) (~ #& . 7) (X #& . 12) (U #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 23 .) ((((∀ X Y)) (¬ (ATOM (~ X Y)))) . (AXIOM (TM& ((∀ X Y)) (¬ (ATOM (~ X Y))))) . NIL . ((Y #& . 17) (X #& . 12) (~ #& . 7) (ATOM #& . 2)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 21 .) (NIL . (DECL (NNIL) (OT& . GROUND) CONSTANT LISTP) . NIL . ((NNIL #& . 60) (LISTP #& . 28)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 5 .) (CONSTANT . GROUND . LISTP . NIL . NIL . (#& . 61) . NNIL .) ((NULL NNIL) . (AXIOM (TM& NULL NNIL)) . NIL . ((NNIL #& . 60) (NULL #& . 4)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 17 .) ((((∀ X U)) (LISTP (~ X U))) . (AXIOM (TM& ((∀ X U)) (LISTP (~ X U)))) . NIL . ((LISTP #& . 45) (~ #& . 7) (X #& . 12) (U #& . 19)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 14 .) (1 . * . INFIX . 840 .) (NIL . (DECL (*) (FT& ((GROUND GROUND) GROUND NIL . GROUND)) FUNCTIONAL NIL INFIX 840 BOTH) . NIL . NIL . ((* #& . 55)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 50 .) (FUNCTIONAL . (((GROUND GROUND) GROUND NIL . GROUND)) . UNIVERSAL . BOTH . (#& . 57) . (#& . 56) . * .) ((((∀ U V)) (LISTP (* U V))) . (AXIOM (TM& ((∀ U V)) (LISTP (* U V)))) . NIL . ((V #& . 32) (U #& . 19) (LISTP #& . 45)) . ((* #& . 55)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 51 .) (8 . |REVERSE | . UNARY . 950 .) (NIL . (DECL (REVERSE) (OT& (GROUND) . GROUND) CONSTANT NIL UNARY 950) . NIL . ((REVERSE #& . 51)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 66 .) (CONSTANT . ((GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 53) . (#& . 52) . REVERSE .) ((((∀ U)) (LISTP (REVERSE U))) . (AXIOM (TM& ((∀ U)) (LISTP (REVERSE U)))) . NIL . ((U #& . 19) (LISTP #& . 45) (REVERSE #& . 51)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 67 .) ((((∀ X Y Z)) (LISTP (LIST X Y Z))) . (AXIOM (TM& ((∀ X Y Z)) (LISTP (LIST X Y Z)))) . NIL . ((Y #& . 17) (X #& . 12) (Z #& . 14) (LISTP #& . 45)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 46 .) ((((∀ X Y)) (LISTP (LIST X Y))) . (AXIOM (TM& ((∀ X Y)) (LISTP (LIST X Y)))) . NIL . ((Y #& . 17) (X #& . 12) (LISTP #& . 45)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 42 .) (6 . |LISTP | . UNARY . 750 .) (NIL . (DECL (LISTP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((LISTP #& . 45)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 10 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 47) . (#& . 46) . LISTP .) (4 . LIST . PREFIX . 1000 .) (NIL . (DECL (LIST) (FT& ((GROUND) GROUND NIL . GROUND)) FUNCTIONAL) . NIL . NIL . ((LIST #& . 42)) . NIL . NIL . NIL . LISPAX . NIL . NIL . 37 .) (FUNCTIONAL . (((GROUND) GROUND NIL . GROUND)) . UNIVERSAL . NIL . (#& . 44) . (#& . 43) . LIST .) ((((∀ X)) (LISTP (LIST X))) . (AXIOM (TM& ((∀ X)) (LISTP (LIST X)))) . NIL . ((X #& . 12) (LISTP #& . 45)) . ((LIST #& . 42)) . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 38 .) ((((∀ X Y)) (SEXP (~ X Y))) . (AXIOM (TM& ((∀ X Y)) (SEXP (~ X Y)))) . NIL . ((SEXP #& . 37) (~ #& . 7) (X #& . 12) (Y #& . 17)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 19 .) (5 . |SEXP | . UNARY . 750 .) (NIL . (DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((SEXP #& . 37)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 11 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 39) . (#& . 38) . SEXP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . W2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . W0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . V3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . V1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . V .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . U2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . U0 .) (5 . LISTP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 29) . (#& . 20) . LISTP .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . U1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . U3 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . V0 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . V2 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . W .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . W1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . W3 .) (NIL . (DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) (OT& . GROUND) VARIABLE LISTP) . NIL . ((W3 #& . 21) (W1 #& . 22) (W #& . 23) (V2 #& . 24) (V0 #& . 25) (U3 #& . 26) (U1 #& . 27) (U #& . 19) (LISTP #& . 28) (U0 #& . 30) (U2 #& . 31) (V #& . 32) (V1 #& . 33) (V3 #& . 34) (W0 #& . 35) (W2 #& . 36)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 1 .) (VARIABLE . GROUND . LISTP . NIL . NIL . (#& . 20) . U .) ((((∀ U)) (SEXP U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((U #& . 19) (SEXP #& . 37)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 12 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 13) . Y .) (4 . SEXP . PREFIX . 1000 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 16) . (#& . 13) . SEXP .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 13) . Z .) (NIL . (DECL (X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Z #& . 14) (X #& . 12) (SEXP #& . 15) (Y #& . 17)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 2 .) (VARIABLE . GROUND . SEXP . NIL . NIL . (#& . 13) . X .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) . NIL . ((PHI #& . 10)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 4 .) (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . (#& . 11) . PHI .) (1 . ~ . INFIX . 850 .) (NIL . (DECL (~) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL INFIX 850) . NIL . ((~ #& . 7)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 7 .) (CONSTANT . ((GROUND GROUND) . GROUND) . UNIVERSAL . NIL . (#& . 9) . (#& . 8) . ~ .) (5 . |ATOM | . UNARY . 750 .) (5 . |NULL | . UNARY . 750 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 5) . (#& . 3) . NULL .) (NIL . (DECL (ATOM NULL) (OT& (GROUND) . TRUTHVAL) CONSTANT NIL UNARY 750) . NIL . ((NULL #& . 4) (ATOM #& . 2)) . NIL . NIL . NIL . NIL . LISPAX . NIL . NIL . 9 .) (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 6) . (#& . 3) . ATOM .) ((((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧ (((∀ X)) (⊃ (ATOM X) (PHI X))) (((∀ X Y)) (⊃ (∧ (PHI X) (PHI Y)) (PHI (~ X Y))))) (((∀ X)) (PHI X))))) . NIL . ((ATOM #& . 2) (~ #& . 7) (PHI #& . 10) (X #& . 12) (Y #& . 17)) . NIL . NIL . ((&& . 1)) . NIL . LISPAX . NIL . NIL . 35 .) ((((∀ X)) (LISTP (FLATTEN X))) . (∀E PHI (TM& ((λ X)) (LISTP (FLATTEN X))) (LN& #& . 1) (MODE& * (STANDARD) ((PART ((1 1 1))) * ($ LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) (STANDARD) ((PART ((1 1 2))) * (& LR& (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) (STANDARD) (REC LR& (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77)) (STANDARD)) ((PART ((1 1))) * (IMP LR& (#& . 54)) (DER)) (STANDARD)) (LR& (#& . 18) (#& . 58) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 54) (#& . 50))) . NIL . ((X #& . 12) (LISTP #& . 45) (FLATTEN #& . 97)) . NIL . NIL . ((#& . 1) (#& . 18) (#& . 40) (#& . 41) (#& . 48) (#& . 49) (#& . 50) (#& . 54) (#& . 58) (#& . 59) (#& . 62) (#& . 63) (#& . 64) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75) (#& . 76) (#& . 77) (#& . 78) (#& . 79) (#& . 89) (#& . 92) (#& . 93) (#& . 96)) . NIL . FLAT . NIL . NIL . 8 .))